basic
\\[0ex]Inj($A$;$B$;$f$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$a_{1}$, $a_{2}$:$A$. ($f$($a_{1}$) = $f$($a_{2}$)) $\Rightarrow$ ($a_{1}$ = $a_{2}$)